Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

REV2(xs, ys) -> DROPLAST1(xs)
REV2(xs, ys) -> ISEMPTY1(xs)
REV2(xs, ys) -> LAST1(xs)
REV2(xs, ys) -> IF4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
DROPLAST1(cons2(x, cons2(y, ys))) -> DROPLAST1(cons2(y, ys))
REVERSE1(xs) -> REV2(xs, nil)
IF4(false, xs, ys, zs) -> REV2(xs, ys)
APPEND2(cons2(x, xs), ys) -> APPEND2(xs, ys)
REV2(xs, ys) -> APPEND2(ys, last1(xs))
LAST1(cons2(x, cons2(y, ys))) -> LAST1(cons2(y, ys))

The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REV2(xs, ys) -> DROPLAST1(xs)
REV2(xs, ys) -> ISEMPTY1(xs)
REV2(xs, ys) -> LAST1(xs)
REV2(xs, ys) -> IF4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
DROPLAST1(cons2(x, cons2(y, ys))) -> DROPLAST1(cons2(y, ys))
REVERSE1(xs) -> REV2(xs, nil)
IF4(false, xs, ys, zs) -> REV2(xs, ys)
APPEND2(cons2(x, xs), ys) -> APPEND2(xs, ys)
REV2(xs, ys) -> APPEND2(ys, last1(xs))
LAST1(cons2(x, cons2(y, ys))) -> LAST1(cons2(y, ys))

The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 4 SCCs with 5 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND2(cons2(x, xs), ys) -> APPEND2(xs, ys)

The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


APPEND2(cons2(x, xs), ys) -> APPEND2(xs, ys)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( APPEND2(x1, x2) ) = x1 + x2


POL( cons2(x1, x2) ) = x1 + x2 + 1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DROPLAST1(cons2(x, cons2(y, ys))) -> DROPLAST1(cons2(y, ys))

The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


DROPLAST1(cons2(x, cons2(y, ys))) -> DROPLAST1(cons2(y, ys))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = x1 + x2 + 1


POL( DROPLAST1(x1) ) = x1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LAST1(cons2(x, cons2(y, ys))) -> LAST1(cons2(y, ys))

The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


LAST1(cons2(x, cons2(y, ys))) -> LAST1(cons2(y, ys))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( LAST1(x1) ) = x1


POL( cons2(x1, x2) ) = x1 + x2 + 1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REV2(xs, ys) -> IF4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
IF4(false, xs, ys, zs) -> REV2(xs, ys)

The TRS R consists of the following rules:

isEmpty1(nil) -> true
isEmpty1(cons2(x, xs)) -> false
last1(cons2(x, nil)) -> x
last1(cons2(x, cons2(y, ys))) -> last1(cons2(y, ys))
dropLast1(nil) -> nil
dropLast1(cons2(x, nil)) -> nil
dropLast1(cons2(x, cons2(y, ys))) -> cons2(x, dropLast1(cons2(y, ys)))
append2(nil, ys) -> ys
append2(cons2(x, xs), ys) -> cons2(x, append2(xs, ys))
reverse1(xs) -> rev2(xs, nil)
rev2(xs, ys) -> if4(isEmpty1(xs), dropLast1(xs), append2(ys, last1(xs)), ys)
if4(true, xs, ys, zs) -> zs
if4(false, xs, ys, zs) -> rev2(xs, ys)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.